Nuprl Definition : token def 12,41
"$token" is Primitive 
latex

origin